Fix #2396 by removing redundant zero in IsNonAssociativeRing#2410
Fix #2396 by removing redundant zero in IsNonAssociativeRing#2410lexvanderstoep wants to merge 5 commits intoagda:masterfrom
Conversation
|
Thanks for the speedy follow-up on the issue... but the failing CI tests show that replacing the (redundant) explicit field with a definition/manifest field is Issues:
|
|
Thanks for reviewing this so quickly! I was about to mark the PR as a draft to fix the usage of About the change being |
|
I'd definitely go with DRAFT for the time being... |
|
Sounds like a plan! |
JacquesCarette
left a comment
There was a problem hiding this comment.
Approving these changes "on their own" but agree with @jamesmckinna about the breaking aspects.
The zero field in the IsNonAssociativeRing was redundant, and could be replaced with a proof based on the other properties.
Now that we've replaced the field `zero` with a definition, we need to update the usages of `IsNonAssociativeRing`.
23b7da7 to
07cae12
Compare
|
Re: the discussion on #2396 I'd be tempted to take this off |
For the removal of the redundant `zero` parameter in `IsNonAssociativeRing`.
|
@jamesmckinna Updated the PR to be 'ready to go'. I'll tackle the almighty |
The zero field in the IsNonAssociativeRing was redundant, and could be replaced with a proof based on the other properties.